0 Prolog
↳1 PrologToPiTRSProof (⇒, 46 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 301 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 22 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 9 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 PiDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 PiDP
↳31 PiDPToQDPProof (⇒, 9 ms)
↳32 QDP
↳33 QDPSizeChangeProof (⇔, 0 ms)
↳34 YES
↳35 PiDP
↳36 UsableRulesProof (⇔, 0 ms)
↳37 PiDP
↳38 PiDPToQDPProof (⇒, 0 ms)
↳39 QDP
↳40 QDPSizeChangeProof (⇔, 0 ms)
↳41 YES
↳42 PiDP
↳43 UsableRulesProof (⇔, 0 ms)
↳44 PiDP
↳45 PiDPToQDPProof (⇒, 0 ms)
↳46 QDP
↳47 MRRProof (⇔, 25 ms)
↳48 QDP
↳49 PisEmptyProof (⇔, 0 ms)
↳50 YES
queens_in_a(Y) → U1_a(Y, perm_in_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_a(Y, perm_out_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2_a(Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, s(0)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, notEq_in_gg(X, F))
notEq_in_gg(0, s(X)) → notEq_out_gg(0, s(X))
notEq_in_gg(s(X), 0) → notEq_out_gg(s(X), 0)
notEq_in_gg(s(X), s(Y)) → U15_gg(X, Y, notEq_in_gg(X, Y))
U15_gg(X, Y, notEq_out_gg(X, Y)) → notEq_out_gg(s(X), s(Y))
U8_ggg(X, F, T, N, notEq_out_gg(X, F)) → U9_ggg(X, F, T, N, add_in_gga(F, N, FplusN))
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U14_gga(X, Y, Z, add_in_gga(X, Y, Z))
U14_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U9_ggg(X, F, T, N, add_out_gga(F, N, FplusN)) → U10_ggg(X, F, T, N, FplusN, notEq_in_gg(X, FplusN))
U10_ggg(X, F, T, N, FplusN, notEq_out_gg(X, FplusN)) → U11_ggg(X, F, T, N, FplusN, add_in_gga(X, N, XplusN))
U11_ggg(X, F, T, N, FplusN, add_out_gga(X, N, XplusN)) → U12_ggg(X, F, T, N, notEq_in_gg(F, XplusN))
U12_ggg(X, F, T, N, notEq_out_gg(F, XplusN)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, s(N)))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, s(N))) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, s(0))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_a(Y, safe_out_g(Y)) → queens_out_a(Y)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
queens_in_a(Y) → U1_a(Y, perm_in_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_a(Y, perm_out_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2_a(Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, s(0)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, notEq_in_gg(X, F))
notEq_in_gg(0, s(X)) → notEq_out_gg(0, s(X))
notEq_in_gg(s(X), 0) → notEq_out_gg(s(X), 0)
notEq_in_gg(s(X), s(Y)) → U15_gg(X, Y, notEq_in_gg(X, Y))
U15_gg(X, Y, notEq_out_gg(X, Y)) → notEq_out_gg(s(X), s(Y))
U8_ggg(X, F, T, N, notEq_out_gg(X, F)) → U9_ggg(X, F, T, N, add_in_gga(F, N, FplusN))
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U14_gga(X, Y, Z, add_in_gga(X, Y, Z))
U14_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U9_ggg(X, F, T, N, add_out_gga(F, N, FplusN)) → U10_ggg(X, F, T, N, FplusN, notEq_in_gg(X, FplusN))
U10_ggg(X, F, T, N, FplusN, notEq_out_gg(X, FplusN)) → U11_ggg(X, F, T, N, FplusN, add_in_gga(X, N, XplusN))
U11_ggg(X, F, T, N, FplusN, add_out_gga(X, N, XplusN)) → U12_ggg(X, F, T, N, notEq_in_gg(F, XplusN))
U12_ggg(X, F, T, N, notEq_out_gg(F, XplusN)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, s(N)))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, s(N))) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, s(0))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_a(Y, safe_out_g(Y)) → queens_out_a(Y)
QUEENS_IN_A(Y) → U1_A(Y, perm_in_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
QUEENS_IN_A(Y) → PERM_IN_GA(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)
PERM_IN_GA(.(X, Y), .(V, Res)) → U3_GA(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
PERM_IN_GA(.(X, Y), .(V, Res)) → DELETE_IN_AGA(V, .(X, Y), Rest)
DELETE_IN_AGA(X, .(F, T), .(F, R)) → U5_AGA(X, F, T, R, delete_in_aga(X, T, R))
DELETE_IN_AGA(X, .(F, T), .(F, R)) → DELETE_IN_AGA(X, T, R)
U3_GA(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_GA(X, Y, V, Res, perm_in_ga(Rest, Res))
U3_GA(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → PERM_IN_GA(Rest, Res)
U1_A(Y, perm_out_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2_A(Y, safe_in_g(Y))
U1_A(Y, perm_out_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → SAFE_IN_G(Y)
SAFE_IN_G(.(X, Y)) → U6_G(X, Y, noattack_in_ggg(X, Y, s(0)))
SAFE_IN_G(.(X, Y)) → NOATTACK_IN_GGG(X, Y, s(0))
NOATTACK_IN_GGG(X, .(F, T), N) → U8_GGG(X, F, T, N, notEq_in_gg(X, F))
NOATTACK_IN_GGG(X, .(F, T), N) → NOTEQ_IN_GG(X, F)
NOTEQ_IN_GG(s(X), s(Y)) → U15_GG(X, Y, notEq_in_gg(X, Y))
NOTEQ_IN_GG(s(X), s(Y)) → NOTEQ_IN_GG(X, Y)
U8_GGG(X, F, T, N, notEq_out_gg(X, F)) → U9_GGG(X, F, T, N, add_in_gga(F, N, FplusN))
U8_GGG(X, F, T, N, notEq_out_gg(X, F)) → ADD_IN_GGA(F, N, FplusN)
ADD_IN_GGA(s(X), Y, s(Z)) → U14_GGA(X, Y, Z, add_in_gga(X, Y, Z))
ADD_IN_GGA(s(X), Y, s(Z)) → ADD_IN_GGA(X, Y, Z)
U9_GGG(X, F, T, N, add_out_gga(F, N, FplusN)) → U10_GGG(X, F, T, N, FplusN, notEq_in_gg(X, FplusN))
U9_GGG(X, F, T, N, add_out_gga(F, N, FplusN)) → NOTEQ_IN_GG(X, FplusN)
U10_GGG(X, F, T, N, FplusN, notEq_out_gg(X, FplusN)) → U11_GGG(X, F, T, N, FplusN, add_in_gga(X, N, XplusN))
U10_GGG(X, F, T, N, FplusN, notEq_out_gg(X, FplusN)) → ADD_IN_GGA(X, N, XplusN)
U11_GGG(X, F, T, N, FplusN, add_out_gga(X, N, XplusN)) → U12_GGG(X, F, T, N, notEq_in_gg(F, XplusN))
U11_GGG(X, F, T, N, FplusN, add_out_gga(X, N, XplusN)) → NOTEQ_IN_GG(F, XplusN)
U12_GGG(X, F, T, N, notEq_out_gg(F, XplusN)) → U13_GGG(X, F, T, N, noattack_in_ggg(X, T, s(N)))
U12_GGG(X, F, T, N, notEq_out_gg(F, XplusN)) → NOATTACK_IN_GGG(X, T, s(N))
U6_G(X, Y, noattack_out_ggg(X, Y, s(0))) → U7_G(X, Y, safe_in_g(Y))
U6_G(X, Y, noattack_out_ggg(X, Y, s(0))) → SAFE_IN_G(Y)
queens_in_a(Y) → U1_a(Y, perm_in_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_a(Y, perm_out_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2_a(Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, s(0)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, notEq_in_gg(X, F))
notEq_in_gg(0, s(X)) → notEq_out_gg(0, s(X))
notEq_in_gg(s(X), 0) → notEq_out_gg(s(X), 0)
notEq_in_gg(s(X), s(Y)) → U15_gg(X, Y, notEq_in_gg(X, Y))
U15_gg(X, Y, notEq_out_gg(X, Y)) → notEq_out_gg(s(X), s(Y))
U8_ggg(X, F, T, N, notEq_out_gg(X, F)) → U9_ggg(X, F, T, N, add_in_gga(F, N, FplusN))
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U14_gga(X, Y, Z, add_in_gga(X, Y, Z))
U14_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U9_ggg(X, F, T, N, add_out_gga(F, N, FplusN)) → U10_ggg(X, F, T, N, FplusN, notEq_in_gg(X, FplusN))
U10_ggg(X, F, T, N, FplusN, notEq_out_gg(X, FplusN)) → U11_ggg(X, F, T, N, FplusN, add_in_gga(X, N, XplusN))
U11_ggg(X, F, T, N, FplusN, add_out_gga(X, N, XplusN)) → U12_ggg(X, F, T, N, notEq_in_gg(F, XplusN))
U12_ggg(X, F, T, N, notEq_out_gg(F, XplusN)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, s(N)))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, s(N))) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, s(0))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_a(Y, safe_out_g(Y)) → queens_out_a(Y)
QUEENS_IN_A(Y) → U1_A(Y, perm_in_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
QUEENS_IN_A(Y) → PERM_IN_GA(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)
PERM_IN_GA(.(X, Y), .(V, Res)) → U3_GA(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
PERM_IN_GA(.(X, Y), .(V, Res)) → DELETE_IN_AGA(V, .(X, Y), Rest)
DELETE_IN_AGA(X, .(F, T), .(F, R)) → U5_AGA(X, F, T, R, delete_in_aga(X, T, R))
DELETE_IN_AGA(X, .(F, T), .(F, R)) → DELETE_IN_AGA(X, T, R)
U3_GA(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_GA(X, Y, V, Res, perm_in_ga(Rest, Res))
U3_GA(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → PERM_IN_GA(Rest, Res)
U1_A(Y, perm_out_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2_A(Y, safe_in_g(Y))
U1_A(Y, perm_out_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → SAFE_IN_G(Y)
SAFE_IN_G(.(X, Y)) → U6_G(X, Y, noattack_in_ggg(X, Y, s(0)))
SAFE_IN_G(.(X, Y)) → NOATTACK_IN_GGG(X, Y, s(0))
NOATTACK_IN_GGG(X, .(F, T), N) → U8_GGG(X, F, T, N, notEq_in_gg(X, F))
NOATTACK_IN_GGG(X, .(F, T), N) → NOTEQ_IN_GG(X, F)
NOTEQ_IN_GG(s(X), s(Y)) → U15_GG(X, Y, notEq_in_gg(X, Y))
NOTEQ_IN_GG(s(X), s(Y)) → NOTEQ_IN_GG(X, Y)
U8_GGG(X, F, T, N, notEq_out_gg(X, F)) → U9_GGG(X, F, T, N, add_in_gga(F, N, FplusN))
U8_GGG(X, F, T, N, notEq_out_gg(X, F)) → ADD_IN_GGA(F, N, FplusN)
ADD_IN_GGA(s(X), Y, s(Z)) → U14_GGA(X, Y, Z, add_in_gga(X, Y, Z))
ADD_IN_GGA(s(X), Y, s(Z)) → ADD_IN_GGA(X, Y, Z)
U9_GGG(X, F, T, N, add_out_gga(F, N, FplusN)) → U10_GGG(X, F, T, N, FplusN, notEq_in_gg(X, FplusN))
U9_GGG(X, F, T, N, add_out_gga(F, N, FplusN)) → NOTEQ_IN_GG(X, FplusN)
U10_GGG(X, F, T, N, FplusN, notEq_out_gg(X, FplusN)) → U11_GGG(X, F, T, N, FplusN, add_in_gga(X, N, XplusN))
U10_GGG(X, F, T, N, FplusN, notEq_out_gg(X, FplusN)) → ADD_IN_GGA(X, N, XplusN)
U11_GGG(X, F, T, N, FplusN, add_out_gga(X, N, XplusN)) → U12_GGG(X, F, T, N, notEq_in_gg(F, XplusN))
U11_GGG(X, F, T, N, FplusN, add_out_gga(X, N, XplusN)) → NOTEQ_IN_GG(F, XplusN)
U12_GGG(X, F, T, N, notEq_out_gg(F, XplusN)) → U13_GGG(X, F, T, N, noattack_in_ggg(X, T, s(N)))
U12_GGG(X, F, T, N, notEq_out_gg(F, XplusN)) → NOATTACK_IN_GGG(X, T, s(N))
U6_G(X, Y, noattack_out_ggg(X, Y, s(0))) → U7_G(X, Y, safe_in_g(Y))
U6_G(X, Y, noattack_out_ggg(X, Y, s(0))) → SAFE_IN_G(Y)
queens_in_a(Y) → U1_a(Y, perm_in_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_a(Y, perm_out_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2_a(Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, s(0)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, notEq_in_gg(X, F))
notEq_in_gg(0, s(X)) → notEq_out_gg(0, s(X))
notEq_in_gg(s(X), 0) → notEq_out_gg(s(X), 0)
notEq_in_gg(s(X), s(Y)) → U15_gg(X, Y, notEq_in_gg(X, Y))
U15_gg(X, Y, notEq_out_gg(X, Y)) → notEq_out_gg(s(X), s(Y))
U8_ggg(X, F, T, N, notEq_out_gg(X, F)) → U9_ggg(X, F, T, N, add_in_gga(F, N, FplusN))
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U14_gga(X, Y, Z, add_in_gga(X, Y, Z))
U14_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U9_ggg(X, F, T, N, add_out_gga(F, N, FplusN)) → U10_ggg(X, F, T, N, FplusN, notEq_in_gg(X, FplusN))
U10_ggg(X, F, T, N, FplusN, notEq_out_gg(X, FplusN)) → U11_ggg(X, F, T, N, FplusN, add_in_gga(X, N, XplusN))
U11_ggg(X, F, T, N, FplusN, add_out_gga(X, N, XplusN)) → U12_ggg(X, F, T, N, notEq_in_gg(F, XplusN))
U12_ggg(X, F, T, N, notEq_out_gg(F, XplusN)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, s(N)))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, s(N))) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, s(0))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_a(Y, safe_out_g(Y)) → queens_out_a(Y)
ADD_IN_GGA(s(X), Y, s(Z)) → ADD_IN_GGA(X, Y, Z)
queens_in_a(Y) → U1_a(Y, perm_in_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_a(Y, perm_out_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2_a(Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, s(0)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, notEq_in_gg(X, F))
notEq_in_gg(0, s(X)) → notEq_out_gg(0, s(X))
notEq_in_gg(s(X), 0) → notEq_out_gg(s(X), 0)
notEq_in_gg(s(X), s(Y)) → U15_gg(X, Y, notEq_in_gg(X, Y))
U15_gg(X, Y, notEq_out_gg(X, Y)) → notEq_out_gg(s(X), s(Y))
U8_ggg(X, F, T, N, notEq_out_gg(X, F)) → U9_ggg(X, F, T, N, add_in_gga(F, N, FplusN))
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U14_gga(X, Y, Z, add_in_gga(X, Y, Z))
U14_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U9_ggg(X, F, T, N, add_out_gga(F, N, FplusN)) → U10_ggg(X, F, T, N, FplusN, notEq_in_gg(X, FplusN))
U10_ggg(X, F, T, N, FplusN, notEq_out_gg(X, FplusN)) → U11_ggg(X, F, T, N, FplusN, add_in_gga(X, N, XplusN))
U11_ggg(X, F, T, N, FplusN, add_out_gga(X, N, XplusN)) → U12_ggg(X, F, T, N, notEq_in_gg(F, XplusN))
U12_ggg(X, F, T, N, notEq_out_gg(F, XplusN)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, s(N)))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, s(N))) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, s(0))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_a(Y, safe_out_g(Y)) → queens_out_a(Y)
ADD_IN_GGA(s(X), Y, s(Z)) → ADD_IN_GGA(X, Y, Z)
ADD_IN_GGA(s(X), Y) → ADD_IN_GGA(X, Y)
From the DPs we obtained the following set of size-change graphs:
NOTEQ_IN_GG(s(X), s(Y)) → NOTEQ_IN_GG(X, Y)
queens_in_a(Y) → U1_a(Y, perm_in_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_a(Y, perm_out_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2_a(Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, s(0)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, notEq_in_gg(X, F))
notEq_in_gg(0, s(X)) → notEq_out_gg(0, s(X))
notEq_in_gg(s(X), 0) → notEq_out_gg(s(X), 0)
notEq_in_gg(s(X), s(Y)) → U15_gg(X, Y, notEq_in_gg(X, Y))
U15_gg(X, Y, notEq_out_gg(X, Y)) → notEq_out_gg(s(X), s(Y))
U8_ggg(X, F, T, N, notEq_out_gg(X, F)) → U9_ggg(X, F, T, N, add_in_gga(F, N, FplusN))
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U14_gga(X, Y, Z, add_in_gga(X, Y, Z))
U14_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U9_ggg(X, F, T, N, add_out_gga(F, N, FplusN)) → U10_ggg(X, F, T, N, FplusN, notEq_in_gg(X, FplusN))
U10_ggg(X, F, T, N, FplusN, notEq_out_gg(X, FplusN)) → U11_ggg(X, F, T, N, FplusN, add_in_gga(X, N, XplusN))
U11_ggg(X, F, T, N, FplusN, add_out_gga(X, N, XplusN)) → U12_ggg(X, F, T, N, notEq_in_gg(F, XplusN))
U12_ggg(X, F, T, N, notEq_out_gg(F, XplusN)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, s(N)))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, s(N))) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, s(0))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_a(Y, safe_out_g(Y)) → queens_out_a(Y)
NOTEQ_IN_GG(s(X), s(Y)) → NOTEQ_IN_GG(X, Y)
NOTEQ_IN_GG(s(X), s(Y)) → NOTEQ_IN_GG(X, Y)
From the DPs we obtained the following set of size-change graphs:
U8_GGG(X, F, T, N, notEq_out_gg(X, F)) → U9_GGG(X, F, T, N, add_in_gga(F, N, FplusN))
U9_GGG(X, F, T, N, add_out_gga(F, N, FplusN)) → U10_GGG(X, F, T, N, FplusN, notEq_in_gg(X, FplusN))
U10_GGG(X, F, T, N, FplusN, notEq_out_gg(X, FplusN)) → U11_GGG(X, F, T, N, FplusN, add_in_gga(X, N, XplusN))
U11_GGG(X, F, T, N, FplusN, add_out_gga(X, N, XplusN)) → U12_GGG(X, F, T, N, notEq_in_gg(F, XplusN))
U12_GGG(X, F, T, N, notEq_out_gg(F, XplusN)) → NOATTACK_IN_GGG(X, T, s(N))
NOATTACK_IN_GGG(X, .(F, T), N) → U8_GGG(X, F, T, N, notEq_in_gg(X, F))
queens_in_a(Y) → U1_a(Y, perm_in_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_a(Y, perm_out_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2_a(Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, s(0)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, notEq_in_gg(X, F))
notEq_in_gg(0, s(X)) → notEq_out_gg(0, s(X))
notEq_in_gg(s(X), 0) → notEq_out_gg(s(X), 0)
notEq_in_gg(s(X), s(Y)) → U15_gg(X, Y, notEq_in_gg(X, Y))
U15_gg(X, Y, notEq_out_gg(X, Y)) → notEq_out_gg(s(X), s(Y))
U8_ggg(X, F, T, N, notEq_out_gg(X, F)) → U9_ggg(X, F, T, N, add_in_gga(F, N, FplusN))
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U14_gga(X, Y, Z, add_in_gga(X, Y, Z))
U14_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U9_ggg(X, F, T, N, add_out_gga(F, N, FplusN)) → U10_ggg(X, F, T, N, FplusN, notEq_in_gg(X, FplusN))
U10_ggg(X, F, T, N, FplusN, notEq_out_gg(X, FplusN)) → U11_ggg(X, F, T, N, FplusN, add_in_gga(X, N, XplusN))
U11_ggg(X, F, T, N, FplusN, add_out_gga(X, N, XplusN)) → U12_ggg(X, F, T, N, notEq_in_gg(F, XplusN))
U12_ggg(X, F, T, N, notEq_out_gg(F, XplusN)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, s(N)))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, s(N))) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, s(0))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_a(Y, safe_out_g(Y)) → queens_out_a(Y)
U8_GGG(X, F, T, N, notEq_out_gg(X, F)) → U9_GGG(X, F, T, N, add_in_gga(F, N, FplusN))
U9_GGG(X, F, T, N, add_out_gga(F, N, FplusN)) → U10_GGG(X, F, T, N, FplusN, notEq_in_gg(X, FplusN))
U10_GGG(X, F, T, N, FplusN, notEq_out_gg(X, FplusN)) → U11_GGG(X, F, T, N, FplusN, add_in_gga(X, N, XplusN))
U11_GGG(X, F, T, N, FplusN, add_out_gga(X, N, XplusN)) → U12_GGG(X, F, T, N, notEq_in_gg(F, XplusN))
U12_GGG(X, F, T, N, notEq_out_gg(F, XplusN)) → NOATTACK_IN_GGG(X, T, s(N))
NOATTACK_IN_GGG(X, .(F, T), N) → U8_GGG(X, F, T, N, notEq_in_gg(X, F))
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U14_gga(X, Y, Z, add_in_gga(X, Y, Z))
notEq_in_gg(0, s(X)) → notEq_out_gg(0, s(X))
notEq_in_gg(s(X), 0) → notEq_out_gg(s(X), 0)
notEq_in_gg(s(X), s(Y)) → U15_gg(X, Y, notEq_in_gg(X, Y))
U14_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U15_gg(X, Y, notEq_out_gg(X, Y)) → notEq_out_gg(s(X), s(Y))
U8_GGG(X, F, T, N, notEq_out_gg) → U9_GGG(X, F, T, N, add_in_gga(F, N))
U9_GGG(X, F, T, N, add_out_gga(FplusN)) → U10_GGG(X, F, T, N, notEq_in_gg(X, FplusN))
U10_GGG(X, F, T, N, notEq_out_gg) → U11_GGG(X, F, T, N, add_in_gga(X, N))
U11_GGG(X, F, T, N, add_out_gga(XplusN)) → U12_GGG(X, T, N, notEq_in_gg(F, XplusN))
U12_GGG(X, T, N, notEq_out_gg) → NOATTACK_IN_GGG(X, T, s(N))
NOATTACK_IN_GGG(X, .(F, T), N) → U8_GGG(X, F, T, N, notEq_in_gg(X, F))
add_in_gga(0, X) → add_out_gga(X)
add_in_gga(s(X), Y) → U14_gga(add_in_gga(X, Y))
notEq_in_gg(0, s(X)) → notEq_out_gg
notEq_in_gg(s(X), 0) → notEq_out_gg
notEq_in_gg(s(X), s(Y)) → U15_gg(notEq_in_gg(X, Y))
U14_gga(add_out_gga(Z)) → add_out_gga(s(Z))
U15_gg(notEq_out_gg) → notEq_out_gg
add_in_gga(x0, x1)
notEq_in_gg(x0, x1)
U14_gga(x0)
U15_gg(x0)
From the DPs we obtained the following set of size-change graphs:
U6_G(X, Y, noattack_out_ggg(X, Y, s(0))) → SAFE_IN_G(Y)
SAFE_IN_G(.(X, Y)) → U6_G(X, Y, noattack_in_ggg(X, Y, s(0)))
queens_in_a(Y) → U1_a(Y, perm_in_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_a(Y, perm_out_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2_a(Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, s(0)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, notEq_in_gg(X, F))
notEq_in_gg(0, s(X)) → notEq_out_gg(0, s(X))
notEq_in_gg(s(X), 0) → notEq_out_gg(s(X), 0)
notEq_in_gg(s(X), s(Y)) → U15_gg(X, Y, notEq_in_gg(X, Y))
U15_gg(X, Y, notEq_out_gg(X, Y)) → notEq_out_gg(s(X), s(Y))
U8_ggg(X, F, T, N, notEq_out_gg(X, F)) → U9_ggg(X, F, T, N, add_in_gga(F, N, FplusN))
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U14_gga(X, Y, Z, add_in_gga(X, Y, Z))
U14_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U9_ggg(X, F, T, N, add_out_gga(F, N, FplusN)) → U10_ggg(X, F, T, N, FplusN, notEq_in_gg(X, FplusN))
U10_ggg(X, F, T, N, FplusN, notEq_out_gg(X, FplusN)) → U11_ggg(X, F, T, N, FplusN, add_in_gga(X, N, XplusN))
U11_ggg(X, F, T, N, FplusN, add_out_gga(X, N, XplusN)) → U12_ggg(X, F, T, N, notEq_in_gg(F, XplusN))
U12_ggg(X, F, T, N, notEq_out_gg(F, XplusN)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, s(N)))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, s(N))) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, s(0))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_a(Y, safe_out_g(Y)) → queens_out_a(Y)
U6_G(X, Y, noattack_out_ggg(X, Y, s(0))) → SAFE_IN_G(Y)
SAFE_IN_G(.(X, Y)) → U6_G(X, Y, noattack_in_ggg(X, Y, s(0)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, notEq_in_gg(X, F))
U8_ggg(X, F, T, N, notEq_out_gg(X, F)) → U9_ggg(X, F, T, N, add_in_gga(F, N, FplusN))
notEq_in_gg(0, s(X)) → notEq_out_gg(0, s(X))
notEq_in_gg(s(X), 0) → notEq_out_gg(s(X), 0)
notEq_in_gg(s(X), s(Y)) → U15_gg(X, Y, notEq_in_gg(X, Y))
U9_ggg(X, F, T, N, add_out_gga(F, N, FplusN)) → U10_ggg(X, F, T, N, FplusN, notEq_in_gg(X, FplusN))
U15_gg(X, Y, notEq_out_gg(X, Y)) → notEq_out_gg(s(X), s(Y))
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U14_gga(X, Y, Z, add_in_gga(X, Y, Z))
U10_ggg(X, F, T, N, FplusN, notEq_out_gg(X, FplusN)) → U11_ggg(X, F, T, N, FplusN, add_in_gga(X, N, XplusN))
U14_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U11_ggg(X, F, T, N, FplusN, add_out_gga(X, N, XplusN)) → U12_ggg(X, F, T, N, notEq_in_gg(F, XplusN))
U12_ggg(X, F, T, N, notEq_out_gg(F, XplusN)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, s(N)))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, s(N))) → noattack_out_ggg(X, .(F, T), N)
U6_G(Y, noattack_out_ggg) → SAFE_IN_G(Y)
SAFE_IN_G(.(X, Y)) → U6_G(Y, noattack_in_ggg(X, Y, s(0)))
noattack_in_ggg(X, [], N) → noattack_out_ggg
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, notEq_in_gg(X, F))
U8_ggg(X, F, T, N, notEq_out_gg) → U9_ggg(X, F, T, N, add_in_gga(F, N))
notEq_in_gg(0, s(X)) → notEq_out_gg
notEq_in_gg(s(X), 0) → notEq_out_gg
notEq_in_gg(s(X), s(Y)) → U15_gg(notEq_in_gg(X, Y))
U9_ggg(X, F, T, N, add_out_gga(FplusN)) → U10_ggg(X, F, T, N, notEq_in_gg(X, FplusN))
U15_gg(notEq_out_gg) → notEq_out_gg
add_in_gga(0, X) → add_out_gga(X)
add_in_gga(s(X), Y) → U14_gga(add_in_gga(X, Y))
U10_ggg(X, F, T, N, notEq_out_gg) → U11_ggg(X, F, T, N, add_in_gga(X, N))
U14_gga(add_out_gga(Z)) → add_out_gga(s(Z))
U11_ggg(X, F, T, N, add_out_gga(XplusN)) → U12_ggg(X, T, N, notEq_in_gg(F, XplusN))
U12_ggg(X, T, N, notEq_out_gg) → U13_ggg(noattack_in_ggg(X, T, s(N)))
U13_ggg(noattack_out_ggg) → noattack_out_ggg
noattack_in_ggg(x0, x1, x2)
U8_ggg(x0, x1, x2, x3, x4)
notEq_in_gg(x0, x1)
U9_ggg(x0, x1, x2, x3, x4)
U15_gg(x0)
add_in_gga(x0, x1)
U10_ggg(x0, x1, x2, x3, x4)
U14_gga(x0)
U11_ggg(x0, x1, x2, x3, x4)
U12_ggg(x0, x1, x2, x3)
U13_ggg(x0)
From the DPs we obtained the following set of size-change graphs:
DELETE_IN_AGA(X, .(F, T), .(F, R)) → DELETE_IN_AGA(X, T, R)
queens_in_a(Y) → U1_a(Y, perm_in_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_a(Y, perm_out_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2_a(Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, s(0)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, notEq_in_gg(X, F))
notEq_in_gg(0, s(X)) → notEq_out_gg(0, s(X))
notEq_in_gg(s(X), 0) → notEq_out_gg(s(X), 0)
notEq_in_gg(s(X), s(Y)) → U15_gg(X, Y, notEq_in_gg(X, Y))
U15_gg(X, Y, notEq_out_gg(X, Y)) → notEq_out_gg(s(X), s(Y))
U8_ggg(X, F, T, N, notEq_out_gg(X, F)) → U9_ggg(X, F, T, N, add_in_gga(F, N, FplusN))
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U14_gga(X, Y, Z, add_in_gga(X, Y, Z))
U14_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U9_ggg(X, F, T, N, add_out_gga(F, N, FplusN)) → U10_ggg(X, F, T, N, FplusN, notEq_in_gg(X, FplusN))
U10_ggg(X, F, T, N, FplusN, notEq_out_gg(X, FplusN)) → U11_ggg(X, F, T, N, FplusN, add_in_gga(X, N, XplusN))
U11_ggg(X, F, T, N, FplusN, add_out_gga(X, N, XplusN)) → U12_ggg(X, F, T, N, notEq_in_gg(F, XplusN))
U12_ggg(X, F, T, N, notEq_out_gg(F, XplusN)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, s(N)))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, s(N))) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, s(0))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_a(Y, safe_out_g(Y)) → queens_out_a(Y)
DELETE_IN_AGA(X, .(F, T), .(F, R)) → DELETE_IN_AGA(X, T, R)
DELETE_IN_AGA(.(F, T)) → DELETE_IN_AGA(T)
From the DPs we obtained the following set of size-change graphs:
U3_GA(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → PERM_IN_GA(Rest, Res)
PERM_IN_GA(.(X, Y), .(V, Res)) → U3_GA(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
queens_in_a(Y) → U1_a(Y, perm_in_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_a(Y, perm_out_ga(.(s(0), .(s(s(0)), .(s(s(s(0))), .(s(s(s(s(0)))), .(s(s(s(s(s(0))))), .(s(s(s(s(s(s(0)))))), .(s(s(s(s(s(s(s(0))))))), .(s(s(s(s(s(s(s(s(0)))))))), [])))))))), Y)) → U2_a(Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, s(0)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, notEq_in_gg(X, F))
notEq_in_gg(0, s(X)) → notEq_out_gg(0, s(X))
notEq_in_gg(s(X), 0) → notEq_out_gg(s(X), 0)
notEq_in_gg(s(X), s(Y)) → U15_gg(X, Y, notEq_in_gg(X, Y))
U15_gg(X, Y, notEq_out_gg(X, Y)) → notEq_out_gg(s(X), s(Y))
U8_ggg(X, F, T, N, notEq_out_gg(X, F)) → U9_ggg(X, F, T, N, add_in_gga(F, N, FplusN))
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U14_gga(X, Y, Z, add_in_gga(X, Y, Z))
U14_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U9_ggg(X, F, T, N, add_out_gga(F, N, FplusN)) → U10_ggg(X, F, T, N, FplusN, notEq_in_gg(X, FplusN))
U10_ggg(X, F, T, N, FplusN, notEq_out_gg(X, FplusN)) → U11_ggg(X, F, T, N, FplusN, add_in_gga(X, N, XplusN))
U11_ggg(X, F, T, N, FplusN, add_out_gga(X, N, XplusN)) → U12_ggg(X, F, T, N, notEq_in_gg(F, XplusN))
U12_ggg(X, F, T, N, notEq_out_gg(F, XplusN)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, s(N)))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, s(N))) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, s(0))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_a(Y, safe_out_g(Y)) → queens_out_a(Y)
U3_GA(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → PERM_IN_GA(Rest, Res)
PERM_IN_GA(.(X, Y), .(V, Res)) → U3_GA(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_GA(delete_out_aga(V, Rest)) → PERM_IN_GA(Rest)
PERM_IN_GA(.(X, Y)) → U3_GA(delete_in_aga(.(X, Y)))
delete_in_aga(.(X, Y)) → delete_out_aga(X, Y)
delete_in_aga(.(F, T)) → U5_aga(F, delete_in_aga(T))
U5_aga(F, delete_out_aga(X, R)) → delete_out_aga(X, .(F, R))
delete_in_aga(x0)
U5_aga(x0, x1)
U3_GA(delete_out_aga(V, Rest)) → PERM_IN_GA(Rest)
PERM_IN_GA(.(X, Y)) → U3_GA(delete_in_aga(.(X, Y)))
delete_in_aga(.(X, Y)) → delete_out_aga(X, Y)
delete_in_aga(.(F, T)) → U5_aga(F, delete_in_aga(T))
U5_aga(F, delete_out_aga(X, R)) → delete_out_aga(X, .(F, R))
.2 > deleteinaga1 > U5aga2 > U3GA1 > PERMINGA1 > deleteoutaga2
delete_in_aga_1=1
U3_GA_1=1
PERM_IN_GA_1=3
._2=0
delete_out_aga_2=1
U5_aga_2=0
delete_in_aga(x0)
U5_aga(x0, x1)